YES(O(1),O(n^4))
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^4)).
Strict Trs:
{ <(x, y) -> #cklt(#compare(x, y))
, merge(nil(), ys) -> ys
, merge(::(x, xs), nil()) -> ::(x, xs)
, merge(::(x, xs), ::(y, ys)) -> ifmerge(<(x, y), x, xs, y, ys)
, ifmerge(true(), x, xs, y, ys) -> ::(x, merge(xs, ::(y, ys)))
, ifmerge(false(), x, xs, y, ys) -> ::(y, merge(::(x, xs), ys))
, msplit(nil()) -> pair(nil(), nil())
, msplit(::(x, nil())) -> pair(::(x, nil()), nil())
, msplit(::(x, ::(y, ys))) -> msplit'(x, y, msplit(ys))
, msplit'(x, y, pair(xs, ys)) -> pair(::(x, xs), ::(y, ys))
, mergesort(nil()) -> nil()
, mergesort(::(x, nil())) -> ::(x, nil())
, mergesort(::(x, ::(y, ys))) ->
mergesort'(msplit(::(x, ::(y, ys))))
, mergesort'(pair(xs, ys)) -> merge(mergesort(xs), mergesort(ys)) }
Weak Trs:
{ #compare(#0(), #0()) -> #EQ()
, #compare(#0(), #neg(y)) -> #GT()
, #compare(#0(), #pos(y)) -> #LT()
, #compare(#0(), #s(y)) -> #LT()
, #compare(#neg(x), #0()) -> #LT()
, #compare(#neg(x), #neg(y)) -> #compare(y, x)
, #compare(#neg(x), #pos(y)) -> #LT()
, #compare(#pos(x), #0()) -> #GT()
, #compare(#pos(x), #neg(y)) -> #GT()
, #compare(#pos(x), #pos(y)) -> #compare(x, y)
, #compare(#s(x), #0()) -> #GT()
, #compare(#s(x), #s(y)) -> #compare(x, y)
, #cklt(#EQ()) -> #false()
, #cklt(#GT()) -> #false()
, #cklt(#LT()) -> true() }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^4))
We add following dependency tuples:
Strict DPs:
{ <^#(x, y) -> c_1(#cklt^#(#compare(x, y)), #compare^#(x, y))
, merge^#(nil(), ys) -> c_2()
, merge^#(::(x, xs), nil()) -> c_3()
, merge^#(::(x, xs), ::(y, ys)) ->
c_4(ifmerge^#(<(x, y), x, xs, y, ys), <^#(x, y))
, ifmerge^#(true(), x, xs, y, ys) -> c_5(merge^#(xs, ::(y, ys)))
, ifmerge^#(false(), x, xs, y, ys) -> c_6(merge^#(::(x, xs), ys))
, msplit^#(nil()) -> c_7()
, msplit^#(::(x, nil())) -> c_8()
, msplit^#(::(x, ::(y, ys))) ->
c_9(msplit'^#(x, y, msplit(ys)), msplit^#(ys))
, msplit'^#(x, y, pair(xs, ys)) -> c_10()
, mergesort^#(nil()) -> c_11()
, mergesort^#(::(x, nil())) -> c_12()
, mergesort^#(::(x, ::(y, ys))) ->
c_13(mergesort'^#(msplit(::(x, ::(y, ys)))),
msplit^#(::(x, ::(y, ys))))
, mergesort'^#(pair(xs, ys)) ->
c_14(merge^#(mergesort(xs), mergesort(ys)),
mergesort^#(xs),
mergesort^#(ys)) }
Weak DPs:
{ #cklt^#(#EQ()) -> c_27()
, #cklt^#(#GT()) -> c_28()
, #cklt^#(#LT()) -> c_29()
, #compare^#(#0(), #0()) -> c_15()
, #compare^#(#0(), #neg(y)) -> c_16()
, #compare^#(#0(), #pos(y)) -> c_17()
, #compare^#(#0(), #s(y)) -> c_18()
, #compare^#(#neg(x), #0()) -> c_19()
, #compare^#(#neg(x), #neg(y)) -> c_20(#compare^#(y, x))
, #compare^#(#neg(x), #pos(y)) -> c_21()
, #compare^#(#pos(x), #0()) -> c_22()
, #compare^#(#pos(x), #neg(y)) -> c_23()
, #compare^#(#pos(x), #pos(y)) -> c_24(#compare^#(x, y))
, #compare^#(#s(x), #0()) -> c_25()
, #compare^#(#s(x), #s(y)) -> c_26(#compare^#(x, y)) }
and mark the set of starting terms.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^4)).
Strict DPs:
{ <^#(x, y) -> c_1(#cklt^#(#compare(x, y)), #compare^#(x, y))
, merge^#(nil(), ys) -> c_2()
, merge^#(::(x, xs), nil()) -> c_3()
, merge^#(::(x, xs), ::(y, ys)) ->
c_4(ifmerge^#(<(x, y), x, xs, y, ys), <^#(x, y))
, ifmerge^#(true(), x, xs, y, ys) -> c_5(merge^#(xs, ::(y, ys)))
, ifmerge^#(false(), x, xs, y, ys) -> c_6(merge^#(::(x, xs), ys))
, msplit^#(nil()) -> c_7()
, msplit^#(::(x, nil())) -> c_8()
, msplit^#(::(x, ::(y, ys))) ->
c_9(msplit'^#(x, y, msplit(ys)), msplit^#(ys))
, msplit'^#(x, y, pair(xs, ys)) -> c_10()
, mergesort^#(nil()) -> c_11()
, mergesort^#(::(x, nil())) -> c_12()
, mergesort^#(::(x, ::(y, ys))) ->
c_13(mergesort'^#(msplit(::(x, ::(y, ys)))),
msplit^#(::(x, ::(y, ys))))
, mergesort'^#(pair(xs, ys)) ->
c_14(merge^#(mergesort(xs), mergesort(ys)),
mergesort^#(xs),
mergesort^#(ys)) }
Weak DPs:
{ #cklt^#(#EQ()) -> c_27()
, #cklt^#(#GT()) -> c_28()
, #cklt^#(#LT()) -> c_29()
, #compare^#(#0(), #0()) -> c_15()
, #compare^#(#0(), #neg(y)) -> c_16()
, #compare^#(#0(), #pos(y)) -> c_17()
, #compare^#(#0(), #s(y)) -> c_18()
, #compare^#(#neg(x), #0()) -> c_19()
, #compare^#(#neg(x), #neg(y)) -> c_20(#compare^#(y, x))
, #compare^#(#neg(x), #pos(y)) -> c_21()
, #compare^#(#pos(x), #0()) -> c_22()
, #compare^#(#pos(x), #neg(y)) -> c_23()
, #compare^#(#pos(x), #pos(y)) -> c_24(#compare^#(x, y))
, #compare^#(#s(x), #0()) -> c_25()
, #compare^#(#s(x), #s(y)) -> c_26(#compare^#(x, y)) }
Weak Trs:
{ <(x, y) -> #cklt(#compare(x, y))
, #compare(#0(), #0()) -> #EQ()
, #compare(#0(), #neg(y)) -> #GT()
, #compare(#0(), #pos(y)) -> #LT()
, #compare(#0(), #s(y)) -> #LT()
, #compare(#neg(x), #0()) -> #LT()
, #compare(#neg(x), #neg(y)) -> #compare(y, x)
, #compare(#neg(x), #pos(y)) -> #LT()
, #compare(#pos(x), #0()) -> #GT()
, #compare(#pos(x), #neg(y)) -> #GT()
, #compare(#pos(x), #pos(y)) -> #compare(x, y)
, #compare(#s(x), #0()) -> #GT()
, #compare(#s(x), #s(y)) -> #compare(x, y)
, #cklt(#EQ()) -> #false()
, #cklt(#GT()) -> #false()
, #cklt(#LT()) -> true()
, merge(nil(), ys) -> ys
, merge(::(x, xs), nil()) -> ::(x, xs)
, merge(::(x, xs), ::(y, ys)) -> ifmerge(<(x, y), x, xs, y, ys)
, ifmerge(true(), x, xs, y, ys) -> ::(x, merge(xs, ::(y, ys)))
, ifmerge(false(), x, xs, y, ys) -> ::(y, merge(::(x, xs), ys))
, msplit(nil()) -> pair(nil(), nil())
, msplit(::(x, nil())) -> pair(::(x, nil()), nil())
, msplit(::(x, ::(y, ys))) -> msplit'(x, y, msplit(ys))
, msplit'(x, y, pair(xs, ys)) -> pair(::(x, xs), ::(y, ys))
, mergesort(nil()) -> nil()
, mergesort(::(x, nil())) -> ::(x, nil())
, mergesort(::(x, ::(y, ys))) ->
mergesort'(msplit(::(x, ::(y, ys))))
, mergesort'(pair(xs, ys)) -> merge(mergesort(xs), mergesort(ys)) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^4))
We estimate the number of application of {1,2,3,7,8,10,11,12} by
applications of Pre({1,2,3,7,8,10,11,12}) = {4,5,6,9,14}. Here
rules are labeled as follows:
DPs:
{ 1: <^#(x, y) -> c_1(#cklt^#(#compare(x, y)), #compare^#(x, y))
, 2: merge^#(nil(), ys) -> c_2()
, 3: merge^#(::(x, xs), nil()) -> c_3()
, 4: merge^#(::(x, xs), ::(y, ys)) ->
c_4(ifmerge^#(<(x, y), x, xs, y, ys), <^#(x, y))
, 5: ifmerge^#(true(), x, xs, y, ys) -> c_5(merge^#(xs, ::(y, ys)))
, 6: ifmerge^#(false(), x, xs, y, ys) ->
c_6(merge^#(::(x, xs), ys))
, 7: msplit^#(nil()) -> c_7()
, 8: msplit^#(::(x, nil())) -> c_8()
, 9: msplit^#(::(x, ::(y, ys))) ->
c_9(msplit'^#(x, y, msplit(ys)), msplit^#(ys))
, 10: msplit'^#(x, y, pair(xs, ys)) -> c_10()
, 11: mergesort^#(nil()) -> c_11()
, 12: mergesort^#(::(x, nil())) -> c_12()
, 13: mergesort^#(::(x, ::(y, ys))) ->
c_13(mergesort'^#(msplit(::(x, ::(y, ys)))),
msplit^#(::(x, ::(y, ys))))
, 14: mergesort'^#(pair(xs, ys)) ->
c_14(merge^#(mergesort(xs), mergesort(ys)),
mergesort^#(xs),
mergesort^#(ys))
, 15: #cklt^#(#EQ()) -> c_27()
, 16: #cklt^#(#GT()) -> c_28()
, 17: #cklt^#(#LT()) -> c_29()
, 18: #compare^#(#0(), #0()) -> c_15()
, 19: #compare^#(#0(), #neg(y)) -> c_16()
, 20: #compare^#(#0(), #pos(y)) -> c_17()
, 21: #compare^#(#0(), #s(y)) -> c_18()
, 22: #compare^#(#neg(x), #0()) -> c_19()
, 23: #compare^#(#neg(x), #neg(y)) -> c_20(#compare^#(y, x))
, 24: #compare^#(#neg(x), #pos(y)) -> c_21()
, 25: #compare^#(#pos(x), #0()) -> c_22()
, 26: #compare^#(#pos(x), #neg(y)) -> c_23()
, 27: #compare^#(#pos(x), #pos(y)) -> c_24(#compare^#(x, y))
, 28: #compare^#(#s(x), #0()) -> c_25()
, 29: #compare^#(#s(x), #s(y)) -> c_26(#compare^#(x, y)) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^4)).
Strict DPs:
{ merge^#(::(x, xs), ::(y, ys)) ->
c_4(ifmerge^#(<(x, y), x, xs, y, ys), <^#(x, y))
, ifmerge^#(true(), x, xs, y, ys) -> c_5(merge^#(xs, ::(y, ys)))
, ifmerge^#(false(), x, xs, y, ys) -> c_6(merge^#(::(x, xs), ys))
, msplit^#(::(x, ::(y, ys))) ->
c_9(msplit'^#(x, y, msplit(ys)), msplit^#(ys))
, mergesort^#(::(x, ::(y, ys))) ->
c_13(mergesort'^#(msplit(::(x, ::(y, ys)))),
msplit^#(::(x, ::(y, ys))))
, mergesort'^#(pair(xs, ys)) ->
c_14(merge^#(mergesort(xs), mergesort(ys)),
mergesort^#(xs),
mergesort^#(ys)) }
Weak DPs:
{ <^#(x, y) -> c_1(#cklt^#(#compare(x, y)), #compare^#(x, y))
, #cklt^#(#EQ()) -> c_27()
, #cklt^#(#GT()) -> c_28()
, #cklt^#(#LT()) -> c_29()
, #compare^#(#0(), #0()) -> c_15()
, #compare^#(#0(), #neg(y)) -> c_16()
, #compare^#(#0(), #pos(y)) -> c_17()
, #compare^#(#0(), #s(y)) -> c_18()
, #compare^#(#neg(x), #0()) -> c_19()
, #compare^#(#neg(x), #neg(y)) -> c_20(#compare^#(y, x))
, #compare^#(#neg(x), #pos(y)) -> c_21()
, #compare^#(#pos(x), #0()) -> c_22()
, #compare^#(#pos(x), #neg(y)) -> c_23()
, #compare^#(#pos(x), #pos(y)) -> c_24(#compare^#(x, y))
, #compare^#(#s(x), #0()) -> c_25()
, #compare^#(#s(x), #s(y)) -> c_26(#compare^#(x, y))
, merge^#(nil(), ys) -> c_2()
, merge^#(::(x, xs), nil()) -> c_3()
, msplit^#(nil()) -> c_7()
, msplit^#(::(x, nil())) -> c_8()
, msplit'^#(x, y, pair(xs, ys)) -> c_10()
, mergesort^#(nil()) -> c_11()
, mergesort^#(::(x, nil())) -> c_12() }
Weak Trs:
{ <(x, y) -> #cklt(#compare(x, y))
, #compare(#0(), #0()) -> #EQ()
, #compare(#0(), #neg(y)) -> #GT()
, #compare(#0(), #pos(y)) -> #LT()
, #compare(#0(), #s(y)) -> #LT()
, #compare(#neg(x), #0()) -> #LT()
, #compare(#neg(x), #neg(y)) -> #compare(y, x)
, #compare(#neg(x), #pos(y)) -> #LT()
, #compare(#pos(x), #0()) -> #GT()
, #compare(#pos(x), #neg(y)) -> #GT()
, #compare(#pos(x), #pos(y)) -> #compare(x, y)
, #compare(#s(x), #0()) -> #GT()
, #compare(#s(x), #s(y)) -> #compare(x, y)
, #cklt(#EQ()) -> #false()
, #cklt(#GT()) -> #false()
, #cklt(#LT()) -> true()
, merge(nil(), ys) -> ys
, merge(::(x, xs), nil()) -> ::(x, xs)
, merge(::(x, xs), ::(y, ys)) -> ifmerge(<(x, y), x, xs, y, ys)
, ifmerge(true(), x, xs, y, ys) -> ::(x, merge(xs, ::(y, ys)))
, ifmerge(false(), x, xs, y, ys) -> ::(y, merge(::(x, xs), ys))
, msplit(nil()) -> pair(nil(), nil())
, msplit(::(x, nil())) -> pair(::(x, nil()), nil())
, msplit(::(x, ::(y, ys))) -> msplit'(x, y, msplit(ys))
, msplit'(x, y, pair(xs, ys)) -> pair(::(x, xs), ::(y, ys))
, mergesort(nil()) -> nil()
, mergesort(::(x, nil())) -> ::(x, nil())
, mergesort(::(x, ::(y, ys))) ->
mergesort'(msplit(::(x, ::(y, ys))))
, mergesort'(pair(xs, ys)) -> merge(mergesort(xs), mergesort(ys)) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^4))
The following weak DPs constitute a sub-graph of the DG that is
closed under successors. The DPs are removed.
{ <^#(x, y) -> c_1(#cklt^#(#compare(x, y)), #compare^#(x, y))
, #cklt^#(#EQ()) -> c_27()
, #cklt^#(#GT()) -> c_28()
, #cklt^#(#LT()) -> c_29()
, #compare^#(#0(), #0()) -> c_15()
, #compare^#(#0(), #neg(y)) -> c_16()
, #compare^#(#0(), #pos(y)) -> c_17()
, #compare^#(#0(), #s(y)) -> c_18()
, #compare^#(#neg(x), #0()) -> c_19()
, #compare^#(#neg(x), #neg(y)) -> c_20(#compare^#(y, x))
, #compare^#(#neg(x), #pos(y)) -> c_21()
, #compare^#(#pos(x), #0()) -> c_22()
, #compare^#(#pos(x), #neg(y)) -> c_23()
, #compare^#(#pos(x), #pos(y)) -> c_24(#compare^#(x, y))
, #compare^#(#s(x), #0()) -> c_25()
, #compare^#(#s(x), #s(y)) -> c_26(#compare^#(x, y))
, merge^#(nil(), ys) -> c_2()
, merge^#(::(x, xs), nil()) -> c_3()
, msplit^#(nil()) -> c_7()
, msplit^#(::(x, nil())) -> c_8()
, msplit'^#(x, y, pair(xs, ys)) -> c_10()
, mergesort^#(nil()) -> c_11()
, mergesort^#(::(x, nil())) -> c_12() }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^4)).
Strict DPs:
{ merge^#(::(x, xs), ::(y, ys)) ->
c_4(ifmerge^#(<(x, y), x, xs, y, ys), <^#(x, y))
, ifmerge^#(true(), x, xs, y, ys) -> c_5(merge^#(xs, ::(y, ys)))
, ifmerge^#(false(), x, xs, y, ys) -> c_6(merge^#(::(x, xs), ys))
, msplit^#(::(x, ::(y, ys))) ->
c_9(msplit'^#(x, y, msplit(ys)), msplit^#(ys))
, mergesort^#(::(x, ::(y, ys))) ->
c_13(mergesort'^#(msplit(::(x, ::(y, ys)))),
msplit^#(::(x, ::(y, ys))))
, mergesort'^#(pair(xs, ys)) ->
c_14(merge^#(mergesort(xs), mergesort(ys)),
mergesort^#(xs),
mergesort^#(ys)) }
Weak Trs:
{ <(x, y) -> #cklt(#compare(x, y))
, #compare(#0(), #0()) -> #EQ()
, #compare(#0(), #neg(y)) -> #GT()
, #compare(#0(), #pos(y)) -> #LT()
, #compare(#0(), #s(y)) -> #LT()
, #compare(#neg(x), #0()) -> #LT()
, #compare(#neg(x), #neg(y)) -> #compare(y, x)
, #compare(#neg(x), #pos(y)) -> #LT()
, #compare(#pos(x), #0()) -> #GT()
, #compare(#pos(x), #neg(y)) -> #GT()
, #compare(#pos(x), #pos(y)) -> #compare(x, y)
, #compare(#s(x), #0()) -> #GT()
, #compare(#s(x), #s(y)) -> #compare(x, y)
, #cklt(#EQ()) -> #false()
, #cklt(#GT()) -> #false()
, #cklt(#LT()) -> true()
, merge(nil(), ys) -> ys
, merge(::(x, xs), nil()) -> ::(x, xs)
, merge(::(x, xs), ::(y, ys)) -> ifmerge(<(x, y), x, xs, y, ys)
, ifmerge(true(), x, xs, y, ys) -> ::(x, merge(xs, ::(y, ys)))
, ifmerge(false(), x, xs, y, ys) -> ::(y, merge(::(x, xs), ys))
, msplit(nil()) -> pair(nil(), nil())
, msplit(::(x, nil())) -> pair(::(x, nil()), nil())
, msplit(::(x, ::(y, ys))) -> msplit'(x, y, msplit(ys))
, msplit'(x, y, pair(xs, ys)) -> pair(::(x, xs), ::(y, ys))
, mergesort(nil()) -> nil()
, mergesort(::(x, nil())) -> ::(x, nil())
, mergesort(::(x, ::(y, ys))) ->
mergesort'(msplit(::(x, ::(y, ys))))
, mergesort'(pair(xs, ys)) -> merge(mergesort(xs), mergesort(ys)) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^4))
Due to missing edges in the dependency-graph, the right-hand sides
of following rules could be simplified:
{ merge^#(::(x, xs), ::(y, ys)) ->
c_4(ifmerge^#(<(x, y), x, xs, y, ys), <^#(x, y))
, msplit^#(::(x, ::(y, ys))) ->
c_9(msplit'^#(x, y, msplit(ys)), msplit^#(ys)) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^4)).
Strict DPs:
{ merge^#(::(x, xs), ::(y, ys)) ->
c_1(ifmerge^#(<(x, y), x, xs, y, ys))
, ifmerge^#(true(), x, xs, y, ys) -> c_2(merge^#(xs, ::(y, ys)))
, ifmerge^#(false(), x, xs, y, ys) -> c_3(merge^#(::(x, xs), ys))
, msplit^#(::(x, ::(y, ys))) -> c_4(msplit^#(ys))
, mergesort^#(::(x, ::(y, ys))) ->
c_5(mergesort'^#(msplit(::(x, ::(y, ys)))),
msplit^#(::(x, ::(y, ys))))
, mergesort'^#(pair(xs, ys)) ->
c_6(merge^#(mergesort(xs), mergesort(ys)),
mergesort^#(xs),
mergesort^#(ys)) }
Weak Trs:
{ <(x, y) -> #cklt(#compare(x, y))
, #compare(#0(), #0()) -> #EQ()
, #compare(#0(), #neg(y)) -> #GT()
, #compare(#0(), #pos(y)) -> #LT()
, #compare(#0(), #s(y)) -> #LT()
, #compare(#neg(x), #0()) -> #LT()
, #compare(#neg(x), #neg(y)) -> #compare(y, x)
, #compare(#neg(x), #pos(y)) -> #LT()
, #compare(#pos(x), #0()) -> #GT()
, #compare(#pos(x), #neg(y)) -> #GT()
, #compare(#pos(x), #pos(y)) -> #compare(x, y)
, #compare(#s(x), #0()) -> #GT()
, #compare(#s(x), #s(y)) -> #compare(x, y)
, #cklt(#EQ()) -> #false()
, #cklt(#GT()) -> #false()
, #cklt(#LT()) -> true()
, merge(nil(), ys) -> ys
, merge(::(x, xs), nil()) -> ::(x, xs)
, merge(::(x, xs), ::(y, ys)) -> ifmerge(<(x, y), x, xs, y, ys)
, ifmerge(true(), x, xs, y, ys) -> ::(x, merge(xs, ::(y, ys)))
, ifmerge(false(), x, xs, y, ys) -> ::(y, merge(::(x, xs), ys))
, msplit(nil()) -> pair(nil(), nil())
, msplit(::(x, nil())) -> pair(::(x, nil()), nil())
, msplit(::(x, ::(y, ys))) -> msplit'(x, y, msplit(ys))
, msplit'(x, y, pair(xs, ys)) -> pair(::(x, xs), ::(y, ys))
, mergesort(nil()) -> nil()
, mergesort(::(x, nil())) -> ::(x, nil())
, mergesort(::(x, ::(y, ys))) ->
mergesort'(msplit(::(x, ::(y, ys))))
, mergesort'(pair(xs, ys)) -> merge(mergesort(xs), mergesort(ys)) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^4))
We use the processor 'matrix interpretation of dimension 1' to
orient following rules strictly.
DPs:
{ 3: ifmerge^#(false(), x, xs, y, ys) ->
c_3(merge^#(::(x, xs), ys)) }
Trs:
{ #compare(#0(), #0()) -> #EQ()
, #compare(#0(), #neg(y)) -> #GT()
, #compare(#0(), #pos(y)) -> #LT()
, #compare(#0(), #s(y)) -> #LT()
, #compare(#neg(x), #0()) -> #LT()
, #compare(#neg(x), #pos(y)) -> #LT()
, #compare(#pos(x), #0()) -> #GT()
, #compare(#pos(x), #neg(y)) -> #GT()
, #compare(#s(x), #0()) -> #GT()
, merge(nil(), ys) -> ys
, merge(::(x, xs), nil()) -> ::(x, xs)
, merge(::(x, xs), ::(y, ys)) -> ifmerge(<(x, y), x, xs, y, ys)
, ifmerge(false(), x, xs, y, ys) -> ::(y, merge(::(x, xs), ys))
, msplit(::(x, nil())) -> pair(::(x, nil()), nil())
, msplit(::(x, ::(y, ys))) -> msplit'(x, y, msplit(ys)) }
Sub-proof:
----------
The following argument positions are usable:
Uargs(c_1) = {1}, Uargs(c_2) = {1}, Uargs(c_3) = {1},
Uargs(c_4) = {1}, Uargs(c_5) = {1, 2}, Uargs(c_6) = {1, 2, 3}
TcT has computed following constructor-restricted matrix
interpretation. Note that the diagonal of the component-wise maxima
of interpretation-entries (of constructors) contains no more than 0
non-zero entries.
[<](x1, x2) = [0]
[#compare](x1, x2) = [1] x2 + [1]
[#cklt](x1) = [0]
[nil] = [0]
[merge](x1, x2) = [1] x1 + [1] x2 + [1]
[::](x1, x2) = [1]
[ifmerge](x1, x2, x3, x4, x5) = [1] x1 + [1]
[true] = [0]
[false] = [1]
[msplit](x1) = [1] x1 + [1]
[pair](x1, x2) = [1]
[msplit'](x1, x2, x3) = [1]
[mergesort](x1) = [1] x1 + [0]
[mergesort'](x1) = [1]
[#EQ] = [1]
[#false] = [0]
[#GT] = [1]
[#LT] = [1]
[#0] = [1]
[#neg](x1) = [1]
[#pos](x1) = [1]
[#s](x1) = [1]
[merge^#](x1, x2) = [0]
[ifmerge^#](x1, x2, x3, x4, x5) = [1] x1 + [0]
[msplit^#](x1) = [0]
[mergesort^#](x1) = [0]
[mergesort'^#](x1) = [0]
[c_1](x1) = [1] x1 + [0]
[c_2](x1) = [1] x1 + [0]
[c_3](x1) = [1] x1 + [0]
[c_4](x1) = [1] x1 + [0]
[c_5](x1, x2) = [1] x1 + [1] x2 + [0]
[c_6](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0]
This order satisfies following ordering constraints
[<(x, y)] = [0]
>= [0]
= [#cklt(#compare(x, y))]
[#cklt(#EQ())] = [0]
>= [0]
= [#false()]
[#cklt(#GT())] = [0]
>= [0]
= [#false()]
[#cklt(#LT())] = [0]
>= [0]
= [true()]
[merge(nil(), ys)] = [1] ys + [1]
> [1] ys + [0]
= [ys]
[merge(::(x, xs), nil())] = [2]
> [1]
= [::(x, xs)]
[merge(::(x, xs), ::(y, ys))] = [3]
> [1]
= [ifmerge(<(x, y), x, xs, y, ys)]
[ifmerge(true(), x, xs, y, ys)] = [1]
>= [1]
= [::(x, merge(xs, ::(y, ys)))]
[ifmerge(false(), x, xs, y, ys)] = [2]
> [1]
= [::(y, merge(::(x, xs), ys))]
[msplit(nil())] = [1]
>= [1]
= [pair(nil(), nil())]
[msplit(::(x, nil()))] = [2]
> [1]
= [pair(::(x, nil()), nil())]
[msplit(::(x, ::(y, ys)))] = [2]
> [1]
= [msplit'(x, y, msplit(ys))]
[msplit'(x, y, pair(xs, ys))] = [1]
>= [1]
= [pair(::(x, xs), ::(y, ys))]
[merge^#(::(x, xs), ::(y, ys))] = [0]
>= [0]
= [c_1(ifmerge^#(<(x, y), x, xs, y, ys))]
[ifmerge^#(true(), x, xs, y, ys)] = [0]
>= [0]
= [c_2(merge^#(xs, ::(y, ys)))]
[ifmerge^#(false(), x, xs, y, ys)] = [1]
> [0]
= [c_3(merge^#(::(x, xs), ys))]
[msplit^#(::(x, ::(y, ys)))] = [0]
>= [0]
= [c_4(msplit^#(ys))]
[mergesort^#(::(x, ::(y, ys)))] = [0]
>= [0]
= [c_5(mergesort'^#(msplit(::(x, ::(y, ys)))),
msplit^#(::(x, ::(y, ys))))]
[mergesort'^#(pair(xs, ys))] = [0]
>= [0]
= [c_6(merge^#(mergesort(xs), mergesort(ys)),
mergesort^#(xs),
mergesort^#(ys))]
The strictly oriented rules are moved into the corresponding weak
component(s).
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^4)).
Strict DPs:
{ merge^#(::(x, xs), ::(y, ys)) ->
c_1(ifmerge^#(<(x, y), x, xs, y, ys))
, ifmerge^#(true(), x, xs, y, ys) -> c_2(merge^#(xs, ::(y, ys)))
, msplit^#(::(x, ::(y, ys))) -> c_4(msplit^#(ys))
, mergesort^#(::(x, ::(y, ys))) ->
c_5(mergesort'^#(msplit(::(x, ::(y, ys)))),
msplit^#(::(x, ::(y, ys))))
, mergesort'^#(pair(xs, ys)) ->
c_6(merge^#(mergesort(xs), mergesort(ys)),
mergesort^#(xs),
mergesort^#(ys)) }
Weak DPs:
{ ifmerge^#(false(), x, xs, y, ys) -> c_3(merge^#(::(x, xs), ys)) }
Weak Trs:
{ <(x, y) -> #cklt(#compare(x, y))
, #compare(#0(), #0()) -> #EQ()
, #compare(#0(), #neg(y)) -> #GT()
, #compare(#0(), #pos(y)) -> #LT()
, #compare(#0(), #s(y)) -> #LT()
, #compare(#neg(x), #0()) -> #LT()
, #compare(#neg(x), #neg(y)) -> #compare(y, x)
, #compare(#neg(x), #pos(y)) -> #LT()
, #compare(#pos(x), #0()) -> #GT()
, #compare(#pos(x), #neg(y)) -> #GT()
, #compare(#pos(x), #pos(y)) -> #compare(x, y)
, #compare(#s(x), #0()) -> #GT()
, #compare(#s(x), #s(y)) -> #compare(x, y)
, #cklt(#EQ()) -> #false()
, #cklt(#GT()) -> #false()
, #cklt(#LT()) -> true()
, merge(nil(), ys) -> ys
, merge(::(x, xs), nil()) -> ::(x, xs)
, merge(::(x, xs), ::(y, ys)) -> ifmerge(<(x, y), x, xs, y, ys)
, ifmerge(true(), x, xs, y, ys) -> ::(x, merge(xs, ::(y, ys)))
, ifmerge(false(), x, xs, y, ys) -> ::(y, merge(::(x, xs), ys))
, msplit(nil()) -> pair(nil(), nil())
, msplit(::(x, nil())) -> pair(::(x, nil()), nil())
, msplit(::(x, ::(y, ys))) -> msplit'(x, y, msplit(ys))
, msplit'(x, y, pair(xs, ys)) -> pair(::(x, xs), ::(y, ys))
, mergesort(nil()) -> nil()
, mergesort(::(x, nil())) -> ::(x, nil())
, mergesort(::(x, ::(y, ys))) ->
mergesort'(msplit(::(x, ::(y, ys))))
, mergesort'(pair(xs, ys)) -> merge(mergesort(xs), mergesort(ys)) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^4))
We decompose the input problem according to the dependency graph
into the upper component
{ mergesort^#(::(x, ::(y, ys))) ->
c_5(mergesort'^#(msplit(::(x, ::(y, ys)))),
msplit^#(::(x, ::(y, ys))))
, mergesort'^#(pair(xs, ys)) ->
c_6(merge^#(mergesort(xs), mergesort(ys)),
mergesort^#(xs),
mergesort^#(ys)) }
and lower component
{ merge^#(::(x, xs), ::(y, ys)) ->
c_1(ifmerge^#(<(x, y), x, xs, y, ys))
, ifmerge^#(true(), x, xs, y, ys) -> c_2(merge^#(xs, ::(y, ys)))
, ifmerge^#(false(), x, xs, y, ys) -> c_3(merge^#(::(x, xs), ys))
, msplit^#(::(x, ::(y, ys))) -> c_4(msplit^#(ys)) }
Further, following extension rules are added to the lower
component.
{ mergesort^#(::(x, ::(y, ys))) -> msplit^#(::(x, ::(y, ys)))
, mergesort^#(::(x, ::(y, ys))) ->
mergesort'^#(msplit(::(x, ::(y, ys))))
, mergesort'^#(pair(xs, ys)) ->
merge^#(mergesort(xs), mergesort(ys))
, mergesort'^#(pair(xs, ys)) -> mergesort^#(xs)
, mergesort'^#(pair(xs, ys)) -> mergesort^#(ys) }
TcT solves the upper component with certificate YES(O(1),O(n^3)).
Sub-proof:
----------
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^3)).
Strict DPs:
{ mergesort^#(::(x, ::(y, ys))) ->
c_5(mergesort'^#(msplit(::(x, ::(y, ys)))),
msplit^#(::(x, ::(y, ys))))
, mergesort'^#(pair(xs, ys)) ->
c_6(merge^#(mergesort(xs), mergesort(ys)),
mergesort^#(xs),
mergesort^#(ys)) }
Weak Trs:
{ <(x, y) -> #cklt(#compare(x, y))
, #compare(#0(), #0()) -> #EQ()
, #compare(#0(), #neg(y)) -> #GT()
, #compare(#0(), #pos(y)) -> #LT()
, #compare(#0(), #s(y)) -> #LT()
, #compare(#neg(x), #0()) -> #LT()
, #compare(#neg(x), #neg(y)) -> #compare(y, x)
, #compare(#neg(x), #pos(y)) -> #LT()
, #compare(#pos(x), #0()) -> #GT()
, #compare(#pos(x), #neg(y)) -> #GT()
, #compare(#pos(x), #pos(y)) -> #compare(x, y)
, #compare(#s(x), #0()) -> #GT()
, #compare(#s(x), #s(y)) -> #compare(x, y)
, #cklt(#EQ()) -> #false()
, #cklt(#GT()) -> #false()
, #cklt(#LT()) -> true()
, merge(nil(), ys) -> ys
, merge(::(x, xs), nil()) -> ::(x, xs)
, merge(::(x, xs), ::(y, ys)) -> ifmerge(<(x, y), x, xs, y, ys)
, ifmerge(true(), x, xs, y, ys) -> ::(x, merge(xs, ::(y, ys)))
, ifmerge(false(), x, xs, y, ys) -> ::(y, merge(::(x, xs), ys))
, msplit(nil()) -> pair(nil(), nil())
, msplit(::(x, nil())) -> pair(::(x, nil()), nil())
, msplit(::(x, ::(y, ys))) -> msplit'(x, y, msplit(ys))
, msplit'(x, y, pair(xs, ys)) -> pair(::(x, xs), ::(y, ys))
, mergesort(nil()) -> nil()
, mergesort(::(x, nil())) -> ::(x, nil())
, mergesort(::(x, ::(y, ys))) ->
mergesort'(msplit(::(x, ::(y, ys))))
, mergesort'(pair(xs, ys)) -> merge(mergesort(xs), mergesort(ys)) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^3))
Due to missing edges in the dependency-graph, the right-hand sides
of following rules could be simplified:
{ mergesort^#(::(x, ::(y, ys))) ->
c_5(mergesort'^#(msplit(::(x, ::(y, ys)))),
msplit^#(::(x, ::(y, ys))))
, mergesort'^#(pair(xs, ys)) ->
c_6(merge^#(mergesort(xs), mergesort(ys)),
mergesort^#(xs),
mergesort^#(ys)) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^3)).
Strict DPs:
{ mergesort^#(::(x, ::(y, ys))) ->
c_1(mergesort'^#(msplit(::(x, ::(y, ys)))))
, mergesort'^#(pair(xs, ys)) ->
c_2(mergesort^#(xs), mergesort^#(ys)) }
Weak Trs:
{ <(x, y) -> #cklt(#compare(x, y))
, #compare(#0(), #0()) -> #EQ()
, #compare(#0(), #neg(y)) -> #GT()
, #compare(#0(), #pos(y)) -> #LT()
, #compare(#0(), #s(y)) -> #LT()
, #compare(#neg(x), #0()) -> #LT()
, #compare(#neg(x), #neg(y)) -> #compare(y, x)
, #compare(#neg(x), #pos(y)) -> #LT()
, #compare(#pos(x), #0()) -> #GT()
, #compare(#pos(x), #neg(y)) -> #GT()
, #compare(#pos(x), #pos(y)) -> #compare(x, y)
, #compare(#s(x), #0()) -> #GT()
, #compare(#s(x), #s(y)) -> #compare(x, y)
, #cklt(#EQ()) -> #false()
, #cklt(#GT()) -> #false()
, #cklt(#LT()) -> true()
, merge(nil(), ys) -> ys
, merge(::(x, xs), nil()) -> ::(x, xs)
, merge(::(x, xs), ::(y, ys)) -> ifmerge(<(x, y), x, xs, y, ys)
, ifmerge(true(), x, xs, y, ys) -> ::(x, merge(xs, ::(y, ys)))
, ifmerge(false(), x, xs, y, ys) -> ::(y, merge(::(x, xs), ys))
, msplit(nil()) -> pair(nil(), nil())
, msplit(::(x, nil())) -> pair(::(x, nil()), nil())
, msplit(::(x, ::(y, ys))) -> msplit'(x, y, msplit(ys))
, msplit'(x, y, pair(xs, ys)) -> pair(::(x, xs), ::(y, ys))
, mergesort(nil()) -> nil()
, mergesort(::(x, nil())) -> ::(x, nil())
, mergesort(::(x, ::(y, ys))) ->
mergesort'(msplit(::(x, ::(y, ys))))
, mergesort'(pair(xs, ys)) -> merge(mergesort(xs), mergesort(ys)) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^3))
We replace rewrite rules by usable rules:
Weak Usable Rules:
{ msplit(nil()) -> pair(nil(), nil())
, msplit(::(x, nil())) -> pair(::(x, nil()), nil())
, msplit(::(x, ::(y, ys))) -> msplit'(x, y, msplit(ys))
, msplit'(x, y, pair(xs, ys)) -> pair(::(x, xs), ::(y, ys)) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^3)).
Strict DPs:
{ mergesort^#(::(x, ::(y, ys))) ->
c_1(mergesort'^#(msplit(::(x, ::(y, ys)))))
, mergesort'^#(pair(xs, ys)) ->
c_2(mergesort^#(xs), mergesort^#(ys)) }
Weak Trs:
{ msplit(nil()) -> pair(nil(), nil())
, msplit(::(x, nil())) -> pair(::(x, nil()), nil())
, msplit(::(x, ::(y, ys))) -> msplit'(x, y, msplit(ys))
, msplit'(x, y, pair(xs, ys)) -> pair(::(x, xs), ::(y, ys)) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^3))
We use the processor 'matrix interpretation of dimension 3' to
orient following rules strictly.
DPs:
{ 2: mergesort'^#(pair(xs, ys)) ->
c_2(mergesort^#(xs), mergesort^#(ys)) }
Sub-proof:
----------
The following argument positions are usable:
Uargs(c_1) = {1}, Uargs(c_2) = {1, 2}
TcT has computed following constructor-based matrix interpretation
satisfying not(EDA).
[0]
[nil] = [0]
[0]
[0 0 1] [0]
[::](x1, x2) = [0 1 0] x2 + [1]
[0 1 0] [0]
[0 0 0] [1]
[msplit](x1) = [0 1 0] x1 + [0]
[1 0 0] [0]
[0 0 0] [0 0 0] [1]
[pair](x1, x2) = [0 1 0] x1 + [0 1 0] x2 + [0]
[0 0 1] [0 0 1] [0]
[0 0 0] [1]
[msplit'](x1, x2, x3) = [1 1 0] x3 + [1]
[0 1 0] [0]
[0 0 1] [0]
[mergesort^#](x1) = [0 0 0] x1 + [0]
[0 0 0] [0]
[0 0 1] [1]
[mergesort'^#](x1) = [0 0 0] x1 + [0]
[0 0 0] [0]
[1 0 0] [0]
[c_1](x1) = [0 0 0] x1 + [0]
[0 0 0] [0]
[1 0 0] [1 0 0] [0]
[c_2](x1, x2) = [0 0 0] x1 + [0 0 0] x2 + [0]
[0 0 0] [0 0 0] [0]
This order satisfies following ordering constraints
[msplit(nil())] = [1]
[0]
[0]
>= [1]
[0]
[0]
= [pair(nil(), nil())]
[msplit(::(x, nil()))] = [1]
[1]
[0]
>= [1]
[1]
[0]
= [pair(::(x, nil()), nil())]
[msplit(::(x, ::(y, ys)))] = [0 0 0] [1]
[0 1 0] ys + [2]
[0 1 0] [0]
>= [0 0 0] [1]
[0 1 0] ys + [2]
[0 1 0] [0]
= [msplit'(x, y, msplit(ys))]
[msplit'(x, y, pair(xs, ys))] = [0 0 0] [0 0 0] [1]
[0 1 0] xs + [0 1 0] ys + [2]
[0 1 0] [0 1 0] [0]
>= [0 0 0] [0 0 0] [1]
[0 1 0] xs + [0 1 0] ys + [2]
[0 1 0] [0 1 0] [0]
= [pair(::(x, xs), ::(y, ys))]
[mergesort^#(::(x, ::(y, ys)))] = [0 1 0] [1]
[0 0 0] ys + [0]
[0 0 0] [0]
>= [0 1 0] [1]
[0 0 0] ys + [0]
[0 0 0] [0]
= [c_1(mergesort'^#(msplit(::(x, ::(y, ys)))))]
[mergesort'^#(pair(xs, ys))] = [0 0 1] [0 0 1] [1]
[0 0 0] xs + [0 0 0] ys + [0]
[0 0 0] [0 0 0] [0]
> [0 0 1] [0 0 1] [0]
[0 0 0] xs + [0 0 0] ys + [0]
[0 0 0] [0 0 0] [0]
= [c_2(mergesort^#(xs), mergesort^#(ys))]
Consider the set of all dependency pairs
DPs:
{ 1: mergesort^#(::(x, ::(y, ys))) ->
c_1(mergesort'^#(msplit(::(x, ::(y, ys)))))
, 2: mergesort'^#(pair(xs, ys)) ->
c_2(mergesort^#(xs), mergesort^#(ys)) }
Processor 'matrix interpretation of dimension 3' induces the
complexity certificate YES(?,O(n^3)) on application of dependency
pairs {2}. These cover all (indirect) predecessors of dependency
pairs {1,2}, their number of application is equally bounded. The
dependency pairs are shifted into the corresponding weak
component(s).
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Weak DPs:
{ mergesort^#(::(x, ::(y, ys))) ->
c_1(mergesort'^#(msplit(::(x, ::(y, ys)))))
, mergesort'^#(pair(xs, ys)) ->
c_2(mergesort^#(xs), mergesort^#(ys)) }
Weak Trs:
{ msplit(nil()) -> pair(nil(), nil())
, msplit(::(x, nil())) -> pair(::(x, nil()), nil())
, msplit(::(x, ::(y, ys))) -> msplit'(x, y, msplit(ys))
, msplit'(x, y, pair(xs, ys)) -> pair(::(x, xs), ::(y, ys)) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(1))
The following weak DPs constitute a sub-graph of the DG that is
closed under successors. The DPs are removed.
{ mergesort^#(::(x, ::(y, ys))) ->
c_1(mergesort'^#(msplit(::(x, ::(y, ys)))))
, mergesort'^#(pair(xs, ys)) ->
c_2(mergesort^#(xs), mergesort^#(ys)) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Weak Trs:
{ msplit(nil()) -> pair(nil(), nil())
, msplit(::(x, nil())) -> pair(::(x, nil()), nil())
, msplit(::(x, ::(y, ys))) -> msplit'(x, y, msplit(ys))
, msplit'(x, y, pair(xs, ys)) -> pair(::(x, xs), ::(y, ys)) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(1))
No rule is usable, rules are removed from the input problem.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Rules: Empty
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(1))
Empty rules are trivially bounded
We return to the main proof.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs:
{ merge^#(::(x, xs), ::(y, ys)) ->
c_1(ifmerge^#(<(x, y), x, xs, y, ys))
, ifmerge^#(true(), x, xs, y, ys) -> c_2(merge^#(xs, ::(y, ys)))
, msplit^#(::(x, ::(y, ys))) -> c_4(msplit^#(ys)) }
Weak DPs:
{ ifmerge^#(false(), x, xs, y, ys) -> c_3(merge^#(::(x, xs), ys))
, mergesort^#(::(x, ::(y, ys))) -> msplit^#(::(x, ::(y, ys)))
, mergesort^#(::(x, ::(y, ys))) ->
mergesort'^#(msplit(::(x, ::(y, ys))))
, mergesort'^#(pair(xs, ys)) ->
merge^#(mergesort(xs), mergesort(ys))
, mergesort'^#(pair(xs, ys)) -> mergesort^#(xs)
, mergesort'^#(pair(xs, ys)) -> mergesort^#(ys) }
Weak Trs:
{ <(x, y) -> #cklt(#compare(x, y))
, #compare(#0(), #0()) -> #EQ()
, #compare(#0(), #neg(y)) -> #GT()
, #compare(#0(), #pos(y)) -> #LT()
, #compare(#0(), #s(y)) -> #LT()
, #compare(#neg(x), #0()) -> #LT()
, #compare(#neg(x), #neg(y)) -> #compare(y, x)
, #compare(#neg(x), #pos(y)) -> #LT()
, #compare(#pos(x), #0()) -> #GT()
, #compare(#pos(x), #neg(y)) -> #GT()
, #compare(#pos(x), #pos(y)) -> #compare(x, y)
, #compare(#s(x), #0()) -> #GT()
, #compare(#s(x), #s(y)) -> #compare(x, y)
, #cklt(#EQ()) -> #false()
, #cklt(#GT()) -> #false()
, #cklt(#LT()) -> true()
, merge(nil(), ys) -> ys
, merge(::(x, xs), nil()) -> ::(x, xs)
, merge(::(x, xs), ::(y, ys)) -> ifmerge(<(x, y), x, xs, y, ys)
, ifmerge(true(), x, xs, y, ys) -> ::(x, merge(xs, ::(y, ys)))
, ifmerge(false(), x, xs, y, ys) -> ::(y, merge(::(x, xs), ys))
, msplit(nil()) -> pair(nil(), nil())
, msplit(::(x, nil())) -> pair(::(x, nil()), nil())
, msplit(::(x, ::(y, ys))) -> msplit'(x, y, msplit(ys))
, msplit'(x, y, pair(xs, ys)) -> pair(::(x, xs), ::(y, ys))
, mergesort(nil()) -> nil()
, mergesort(::(x, nil())) -> ::(x, nil())
, mergesort(::(x, ::(y, ys))) ->
mergesort'(msplit(::(x, ::(y, ys))))
, mergesort'(pair(xs, ys)) -> merge(mergesort(xs), mergesort(ys)) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
We use the processor 'matrix interpretation of dimension 1' to
orient following rules strictly.
DPs:
{ 1: merge^#(::(x, xs), ::(y, ys)) ->
c_1(ifmerge^#(<(x, y), x, xs, y, ys))
, 5: mergesort^#(::(x, ::(y, ys))) -> msplit^#(::(x, ::(y, ys))) }
Trs: { mergesort(::(x, nil())) -> ::(x, nil()) }
Sub-proof:
----------
The following argument positions are usable:
Uargs(c_1) = {1}, Uargs(c_2) = {1}, Uargs(c_3) = {1},
Uargs(c_4) = {1}
TcT has computed following constructor-based matrix interpretation
satisfying not(EDA).
[<](x1, x2) = [0]
[#compare](x1, x2) = [0]
[#cklt](x1) = [0]
[nil] = [0]
[merge](x1, x2) = [1] x1 + [1] x2 + [0]
[::](x1, x2) = [1] x2 + [1]
[ifmerge](x1, x2, x3, x4, x5) = [1] x3 + [1] x5 + [2]
[true] = [0]
[false] = [1]
[msplit](x1) = [1] x1 + [0]
[pair](x1, x2) = [1] x1 + [1] x2 + [0]
[msplit'](x1, x2, x3) = [1] x3 + [2]
[mergesort](x1) = [2] x1 + [0]
[mergesort'](x1) = [2] x1 + [0]
[#EQ] = [1]
[#false] = [0]
[#GT] = [1]
[#LT] = [0]
[#0] = [0]
[#neg](x1) = [1] x1 + [0]
[#pos](x1) = [1] x1 + [0]
[#s](x1) = [1] x1 + [0]
[merge^#](x1, x2) = [1] x1 + [0]
[ifmerge^#](x1, x2, x3, x4, x5) = [1] x1 + [1] x3 + [0]
[msplit^#](x1) = [0]
[mergesort^#](x1) = [2] x1 + [0]
[mergesort'^#](x1) = [2] x1 + [0]
[c_1](x1) = [1] x1 + [0]
[c_2](x1) = [1] x1 + [0]
[c_3](x1) = [1] x1 + [0]
[c_4](x1) = [2] x1 + [0]
This order satisfies following ordering constraints
[<(x, y)] = [0]
>= [0]
= [#cklt(#compare(x, y))]
[#cklt(#EQ())] = [0]
>= [0]
= [#false()]
[#cklt(#GT())] = [0]
>= [0]
= [#false()]
[#cklt(#LT())] = [0]
>= [0]
= [true()]
[merge(nil(), ys)] = [1] ys + [0]
>= [1] ys + [0]
= [ys]
[merge(::(x, xs), nil())] = [1] xs + [1]
>= [1] xs + [1]
= [::(x, xs)]
[merge(::(x, xs), ::(y, ys))] = [1] xs + [1] ys + [2]
>= [1] xs + [1] ys + [2]
= [ifmerge(<(x, y), x, xs, y, ys)]
[ifmerge(true(), x, xs, y, ys)] = [1] xs + [1] ys + [2]
>= [1] xs + [1] ys + [2]
= [::(x, merge(xs, ::(y, ys)))]
[ifmerge(false(), x, xs, y, ys)] = [1] xs + [1] ys + [2]
>= [1] xs + [1] ys + [2]
= [::(y, merge(::(x, xs), ys))]
[msplit(nil())] = [0]
>= [0]
= [pair(nil(), nil())]
[msplit(::(x, nil()))] = [1]
>= [1]
= [pair(::(x, nil()), nil())]
[msplit(::(x, ::(y, ys)))] = [1] ys + [2]
>= [1] ys + [2]
= [msplit'(x, y, msplit(ys))]
[msplit'(x, y, pair(xs, ys))] = [1] xs + [1] ys + [2]
>= [1] xs + [1] ys + [2]
= [pair(::(x, xs), ::(y, ys))]
[mergesort(nil())] = [0]
>= [0]
= [nil()]
[mergesort(::(x, nil()))] = [2]
> [1]
= [::(x, nil())]
[mergesort(::(x, ::(y, ys)))] = [2] ys + [4]
>= [2] ys + [4]
= [mergesort'(msplit(::(x, ::(y, ys))))]
[mergesort'(pair(xs, ys))] = [2] xs + [2] ys + [0]
>= [2] xs + [2] ys + [0]
= [merge(mergesort(xs), mergesort(ys))]
[merge^#(::(x, xs), ::(y, ys))] = [1] xs + [1]
> [1] xs + [0]
= [c_1(ifmerge^#(<(x, y), x, xs, y, ys))]
[ifmerge^#(true(), x, xs, y, ys)] = [1] xs + [0]
>= [1] xs + [0]
= [c_2(merge^#(xs, ::(y, ys)))]
[ifmerge^#(false(), x, xs, y, ys)] = [1] xs + [1]
>= [1] xs + [1]
= [c_3(merge^#(::(x, xs), ys))]
[msplit^#(::(x, ::(y, ys)))] = [0]
>= [0]
= [c_4(msplit^#(ys))]
[mergesort^#(::(x, ::(y, ys)))] = [2] ys + [4]
> [0]
= [msplit^#(::(x, ::(y, ys)))]
[mergesort^#(::(x, ::(y, ys)))] = [2] ys + [4]
>= [2] ys + [4]
= [mergesort'^#(msplit(::(x, ::(y, ys))))]
[mergesort'^#(pair(xs, ys))] = [2] xs + [2] ys + [0]
>= [2] xs + [0]
= [merge^#(mergesort(xs), mergesort(ys))]
[mergesort'^#(pair(xs, ys))] = [2] xs + [2] ys + [0]
>= [2] xs + [0]
= [mergesort^#(xs)]
[mergesort'^#(pair(xs, ys))] = [2] xs + [2] ys + [0]
>= [2] ys + [0]
= [mergesort^#(ys)]
Consider the set of all dependency pairs
DPs:
{ 1: merge^#(::(x, xs), ::(y, ys)) ->
c_1(ifmerge^#(<(x, y), x, xs, y, ys))
, 2: ifmerge^#(true(), x, xs, y, ys) -> c_2(merge^#(xs, ::(y, ys)))
, 3: msplit^#(::(x, ::(y, ys))) -> c_4(msplit^#(ys))
, 4: ifmerge^#(false(), x, xs, y, ys) ->
c_3(merge^#(::(x, xs), ys))
, 5: mergesort^#(::(x, ::(y, ys))) -> msplit^#(::(x, ::(y, ys)))
, 6: mergesort^#(::(x, ::(y, ys))) ->
mergesort'^#(msplit(::(x, ::(y, ys))))
, 7: mergesort'^#(pair(xs, ys)) ->
merge^#(mergesort(xs), mergesort(ys))
, 8: mergesort'^#(pair(xs, ys)) -> mergesort^#(xs)
, 9: mergesort'^#(pair(xs, ys)) -> mergesort^#(ys) }
Processor 'matrix interpretation of dimension 1' induces the
complexity certificate YES(?,O(n^1)) on application of dependency
pairs {1,5}. These cover all (indirect) predecessors of dependency
pairs {1,2,4,5}, their number of application is equally bounded.
The dependency pairs are shifted into the corresponding weak
component(s).
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs: { msplit^#(::(x, ::(y, ys))) -> c_4(msplit^#(ys)) }
Weak DPs:
{ merge^#(::(x, xs), ::(y, ys)) ->
c_1(ifmerge^#(<(x, y), x, xs, y, ys))
, ifmerge^#(true(), x, xs, y, ys) -> c_2(merge^#(xs, ::(y, ys)))
, ifmerge^#(false(), x, xs, y, ys) -> c_3(merge^#(::(x, xs), ys))
, mergesort^#(::(x, ::(y, ys))) -> msplit^#(::(x, ::(y, ys)))
, mergesort^#(::(x, ::(y, ys))) ->
mergesort'^#(msplit(::(x, ::(y, ys))))
, mergesort'^#(pair(xs, ys)) ->
merge^#(mergesort(xs), mergesort(ys))
, mergesort'^#(pair(xs, ys)) -> mergesort^#(xs)
, mergesort'^#(pair(xs, ys)) -> mergesort^#(ys) }
Weak Trs:
{ <(x, y) -> #cklt(#compare(x, y))
, #compare(#0(), #0()) -> #EQ()
, #compare(#0(), #neg(y)) -> #GT()
, #compare(#0(), #pos(y)) -> #LT()
, #compare(#0(), #s(y)) -> #LT()
, #compare(#neg(x), #0()) -> #LT()
, #compare(#neg(x), #neg(y)) -> #compare(y, x)
, #compare(#neg(x), #pos(y)) -> #LT()
, #compare(#pos(x), #0()) -> #GT()
, #compare(#pos(x), #neg(y)) -> #GT()
, #compare(#pos(x), #pos(y)) -> #compare(x, y)
, #compare(#s(x), #0()) -> #GT()
, #compare(#s(x), #s(y)) -> #compare(x, y)
, #cklt(#EQ()) -> #false()
, #cklt(#GT()) -> #false()
, #cklt(#LT()) -> true()
, merge(nil(), ys) -> ys
, merge(::(x, xs), nil()) -> ::(x, xs)
, merge(::(x, xs), ::(y, ys)) -> ifmerge(<(x, y), x, xs, y, ys)
, ifmerge(true(), x, xs, y, ys) -> ::(x, merge(xs, ::(y, ys)))
, ifmerge(false(), x, xs, y, ys) -> ::(y, merge(::(x, xs), ys))
, msplit(nil()) -> pair(nil(), nil())
, msplit(::(x, nil())) -> pair(::(x, nil()), nil())
, msplit(::(x, ::(y, ys))) -> msplit'(x, y, msplit(ys))
, msplit'(x, y, pair(xs, ys)) -> pair(::(x, xs), ::(y, ys))
, mergesort(nil()) -> nil()
, mergesort(::(x, nil())) -> ::(x, nil())
, mergesort(::(x, ::(y, ys))) ->
mergesort'(msplit(::(x, ::(y, ys))))
, mergesort'(pair(xs, ys)) -> merge(mergesort(xs), mergesort(ys)) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
The following weak DPs constitute a sub-graph of the DG that is
closed under successors. The DPs are removed.
{ merge^#(::(x, xs), ::(y, ys)) ->
c_1(ifmerge^#(<(x, y), x, xs, y, ys))
, ifmerge^#(true(), x, xs, y, ys) -> c_2(merge^#(xs, ::(y, ys)))
, ifmerge^#(false(), x, xs, y, ys) -> c_3(merge^#(::(x, xs), ys))
, mergesort'^#(pair(xs, ys)) ->
merge^#(mergesort(xs), mergesort(ys)) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs: { msplit^#(::(x, ::(y, ys))) -> c_4(msplit^#(ys)) }
Weak DPs:
{ mergesort^#(::(x, ::(y, ys))) -> msplit^#(::(x, ::(y, ys)))
, mergesort^#(::(x, ::(y, ys))) ->
mergesort'^#(msplit(::(x, ::(y, ys))))
, mergesort'^#(pair(xs, ys)) -> mergesort^#(xs)
, mergesort'^#(pair(xs, ys)) -> mergesort^#(ys) }
Weak Trs:
{ <(x, y) -> #cklt(#compare(x, y))
, #compare(#0(), #0()) -> #EQ()
, #compare(#0(), #neg(y)) -> #GT()
, #compare(#0(), #pos(y)) -> #LT()
, #compare(#0(), #s(y)) -> #LT()
, #compare(#neg(x), #0()) -> #LT()
, #compare(#neg(x), #neg(y)) -> #compare(y, x)
, #compare(#neg(x), #pos(y)) -> #LT()
, #compare(#pos(x), #0()) -> #GT()
, #compare(#pos(x), #neg(y)) -> #GT()
, #compare(#pos(x), #pos(y)) -> #compare(x, y)
, #compare(#s(x), #0()) -> #GT()
, #compare(#s(x), #s(y)) -> #compare(x, y)
, #cklt(#EQ()) -> #false()
, #cklt(#GT()) -> #false()
, #cklt(#LT()) -> true()
, merge(nil(), ys) -> ys
, merge(::(x, xs), nil()) -> ::(x, xs)
, merge(::(x, xs), ::(y, ys)) -> ifmerge(<(x, y), x, xs, y, ys)
, ifmerge(true(), x, xs, y, ys) -> ::(x, merge(xs, ::(y, ys)))
, ifmerge(false(), x, xs, y, ys) -> ::(y, merge(::(x, xs), ys))
, msplit(nil()) -> pair(nil(), nil())
, msplit(::(x, nil())) -> pair(::(x, nil()), nil())
, msplit(::(x, ::(y, ys))) -> msplit'(x, y, msplit(ys))
, msplit'(x, y, pair(xs, ys)) -> pair(::(x, xs), ::(y, ys))
, mergesort(nil()) -> nil()
, mergesort(::(x, nil())) -> ::(x, nil())
, mergesort(::(x, ::(y, ys))) ->
mergesort'(msplit(::(x, ::(y, ys))))
, mergesort'(pair(xs, ys)) -> merge(mergesort(xs), mergesort(ys)) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
We replace rewrite rules by usable rules:
Weak Usable Rules:
{ msplit(nil()) -> pair(nil(), nil())
, msplit(::(x, nil())) -> pair(::(x, nil()), nil())
, msplit(::(x, ::(y, ys))) -> msplit'(x, y, msplit(ys))
, msplit'(x, y, pair(xs, ys)) -> pair(::(x, xs), ::(y, ys)) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs: { msplit^#(::(x, ::(y, ys))) -> c_4(msplit^#(ys)) }
Weak DPs:
{ mergesort^#(::(x, ::(y, ys))) -> msplit^#(::(x, ::(y, ys)))
, mergesort^#(::(x, ::(y, ys))) ->
mergesort'^#(msplit(::(x, ::(y, ys))))
, mergesort'^#(pair(xs, ys)) -> mergesort^#(xs)
, mergesort'^#(pair(xs, ys)) -> mergesort^#(ys) }
Weak Trs:
{ msplit(nil()) -> pair(nil(), nil())
, msplit(::(x, nil())) -> pair(::(x, nil()), nil())
, msplit(::(x, ::(y, ys))) -> msplit'(x, y, msplit(ys))
, msplit'(x, y, pair(xs, ys)) -> pair(::(x, xs), ::(y, ys)) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
We use the processor 'matrix interpretation of dimension 1' to
orient following rules strictly.
DPs:
{ 1: msplit^#(::(x, ::(y, ys))) -> c_4(msplit^#(ys)) }
Sub-proof:
----------
The following argument positions are usable:
Uargs(c_4) = {1}
TcT has computed following constructor-based matrix interpretation
satisfying not(EDA).
[<](x1, x2) = [1] x1 + [1] x2 + [0]
[#compare](x1, x2) = [1] x1 + [1] x2 + [0]
[#cklt](x1) = [1] x1 + [0]
[nil] = [0]
[merge](x1, x2) = [1] x1 + [1] x2 + [0]
[::](x1, x2) = [1] x1 + [1] x2 + [1]
[ifmerge](x1, x2, x3, x4, x5) = [1] x1 + [1] x2 + [1] x3 + [1] x4 + [1] x5 + [0]
[true] = [0]
[false] = [0]
[msplit](x1) = [1] x1 + [0]
[pair](x1, x2) = [1] x1 + [1] x2 + [0]
[msplit'](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [2]
[mergesort](x1) = [1] x1 + [0]
[mergesort'](x1) = [1] x1 + [0]
[#EQ] = [0]
[#false] = [0]
[#GT] = [0]
[#LT] = [0]
[#0] = [0]
[#neg](x1) = [1] x1 + [0]
[#pos](x1) = [1] x1 + [0]
[#s](x1) = [1] x1 + [0]
[merge^#](x1, x2) = [1] x1 + [1] x2 + [0]
[ifmerge^#](x1, x2, x3, x4, x5) = [1] x1 + [1] x2 + [1] x3 + [1] x4 + [1] x5 + [0]
[msplit^#](x1) = [2] x1 + [0]
[mergesort^#](x1) = [2] x1 + [0]
[mergesort'^#](x1) = [2] x1 + [0]
[c_1](x1) = [1] x1 + [0]
[c_2](x1) = [1] x1 + [0]
[c_3](x1) = [1] x1 + [0]
[c_4](x1) = [1] x1 + [0]
This order satisfies following ordering constraints
[msplit(nil())] = [0]
>= [0]
= [pair(nil(), nil())]
[msplit(::(x, nil()))] = [1] x + [1]
>= [1] x + [1]
= [pair(::(x, nil()), nil())]
[msplit(::(x, ::(y, ys)))] = [1] x + [1] y + [1] ys + [2]
>= [1] x + [1] y + [1] ys + [2]
= [msplit'(x, y, msplit(ys))]
[msplit'(x, y, pair(xs, ys))] = [1] x + [1] xs + [1] y + [1] ys + [2]
>= [1] x + [1] xs + [1] y + [1] ys + [2]
= [pair(::(x, xs), ::(y, ys))]
[msplit^#(::(x, ::(y, ys)))] = [2] x + [2] y + [2] ys + [4]
> [2] ys + [0]
= [c_4(msplit^#(ys))]
[mergesort^#(::(x, ::(y, ys)))] = [2] x + [2] y + [2] ys + [4]
>= [2] x + [2] y + [2] ys + [4]
= [msplit^#(::(x, ::(y, ys)))]
[mergesort^#(::(x, ::(y, ys)))] = [2] x + [2] y + [2] ys + [4]
>= [2] x + [2] y + [2] ys + [4]
= [mergesort'^#(msplit(::(x, ::(y, ys))))]
[mergesort'^#(pair(xs, ys))] = [2] xs + [2] ys + [0]
>= [2] xs + [0]
= [mergesort^#(xs)]
[mergesort'^#(pair(xs, ys))] = [2] xs + [2] ys + [0]
>= [2] ys + [0]
= [mergesort^#(ys)]
The strictly oriented rules are moved into the corresponding weak
component(s).
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Weak DPs:
{ msplit^#(::(x, ::(y, ys))) -> c_4(msplit^#(ys))
, mergesort^#(::(x, ::(y, ys))) -> msplit^#(::(x, ::(y, ys)))
, mergesort^#(::(x, ::(y, ys))) ->
mergesort'^#(msplit(::(x, ::(y, ys))))
, mergesort'^#(pair(xs, ys)) -> mergesort^#(xs)
, mergesort'^#(pair(xs, ys)) -> mergesort^#(ys) }
Weak Trs:
{ msplit(nil()) -> pair(nil(), nil())
, msplit(::(x, nil())) -> pair(::(x, nil()), nil())
, msplit(::(x, ::(y, ys))) -> msplit'(x, y, msplit(ys))
, msplit'(x, y, pair(xs, ys)) -> pair(::(x, xs), ::(y, ys)) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(1))
The following weak DPs constitute a sub-graph of the DG that is
closed under successors. The DPs are removed.
{ msplit^#(::(x, ::(y, ys))) -> c_4(msplit^#(ys))
, mergesort^#(::(x, ::(y, ys))) -> msplit^#(::(x, ::(y, ys)))
, mergesort^#(::(x, ::(y, ys))) ->
mergesort'^#(msplit(::(x, ::(y, ys))))
, mergesort'^#(pair(xs, ys)) -> mergesort^#(xs)
, mergesort'^#(pair(xs, ys)) -> mergesort^#(ys) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Weak Trs:
{ msplit(nil()) -> pair(nil(), nil())
, msplit(::(x, nil())) -> pair(::(x, nil()), nil())
, msplit(::(x, ::(y, ys))) -> msplit'(x, y, msplit(ys))
, msplit'(x, y, pair(xs, ys)) -> pair(::(x, xs), ::(y, ys)) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(1))
No rule is usable, rules are removed from the input problem.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Rules: Empty
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(1))
Empty rules are trivially bounded
Wall-time: 102.933846s
CPU-time: 1424.878386s
Hurray, we answered YES(O(1),O(n^4))